A, B:Realizer. A  R-plus(A;B) 

latex

Definitions	True, ff, tt, P  Q, if b then t else f fi , , t  T, let x = a in b(x), R-plus(A;B), x:A. B(x), P & Q, P  Q, Unit, ,
Lemmas	Rnone-implies, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, R-sub-plus-left, R-sub-self, not wf, bnot wf, assert wf, bool wf, Rnone? wf, es realizer wf